$\forall$$A$, $B$:Type, $d$:EqDecider($B$). strong{-}subtype($A$;$B$) $\Rightarrow$ $d$ $\in$ EqDecider($A$)